T:Type, eq:EqDecider(T), a:T, L:(T List).
(b:T. (b  insert(eq; a; L))  ((b = a)  (b  L)))
 (no_repeats(T; L)  no_repeats(T; insert(eq; a; L))) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), no_repeats(T; l), (x  l), prop{i:l}, P  Q, insert(eq; a; L), P  Q, P  Q, P  Q, P  Q, A, hd(l), i <z j, i z j, l[i], b, Unit, , tl(l), b, if b then t else f fi , nth_tl(n;as), Y, ||as||, A  B, , deq-member(eq; x; L), guard(T), True, T
Lemmas	no repeats cons, squash wf, true wf, cons member, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, insert wf, l member wf, no repeats wf, deq wf